Nuprl Definition : ecl-mng-update 11,40

ecl-mng-update{i:l}
ecl-mng-update(es; i; ds; da; x; z; upd)
== es-decls(es;i;ds;da)
==  alle-at(es;
==  alle-at(i;
==  alle-at(e.(es-after(es; z; e)
==  alle-at(e.(=
==  alle-at(e.(list_accum(z',nf.let n,f = nf
==  alle-at(e.(list_accum(in
==  alle-at(e.(list_accum(if es-bact{i:l}
==  alle-at(e.(list_accum(if es-bact(ds; da; x; es; n; es-init(es;e); e)
==  alle-at(e.(list_accum(then f(es-state-when(es; e),es-val(es; e))
==  alle-at(e.(list_accum(else z'
==  alle-at(e.(list_accum(fi ;
==  alle-at(e.(list_accum(es-when(es; z; e);
==  alle-at(e.(list_accum(fpf-cap(upd;
==  alle-at(e.(list_accum(fpf-cap(product-deq(Knd; Id; Kind-deq; id-deq);
==  alle-at(e.(list_accum(fpf-cap(<es-kind(es; e), z>;
==  alle-at(e.(list_accum(fpf-cap([])))) 
latex



clarification:

ecl-mng-update{i:l}
ecl-mng-update(es; i; ds; da; x; z; upd)
== es-decls(es;i;ds;da)
==  alle-at(es;
==  alle-at(i;
==  alle-at(e.(es-after(es; z; e)
==  alle-at(e.(=
==  alle-at(e.(list_accum(z',nf.let n,f = nf
==  alle-at(e.(list_accum(in
==  alle-at(e.(list_accum(if es-bact{i:l}
==  alle-at(e.(list_accum(if es-bact(ds; da; x; es; n; es-init(es;e); e)
==  alle-at(e.(list_accum(then f(es-state-when(es; e),es-val(es; e))
==  alle-at(e.(list_accum(else z'
==  alle-at(e.(list_accum(fi ;
==  alle-at(e.(list_accum(es-when(es; z; e);
==  alle-at(e.(list_accum(fpf-cap(upd;
==  alle-at(e.(list_accum(fpf-cap(product-deq(Knd; Id; Kind-deq; id-deq);
==  alle-at(e.(list_accum(fpf-cap(<es-kind(es; e), z>;
==  alle-at(e.(list_accum(fpf-cap([]))
==  alle-at(e.( fpf-cap(ds; id-deq; z; top))) 
latex


Definitions[], es-kind(es; e), <a, b>, id-deq, Kind-deq, Id, Knd, product-deq(A; B; a; b), fpf-cap(f; eq; x; z), es-when(es; x; e), es-val(es; e), es-state-when(es; e), f(a), es-init(es;e), es-bact{i:l}(ds; da; a; es; n; e1; e2), if b then t else f fi , let x,y = A in B(x;y), list_accum(x,a.f(x;a); y; l), es-after(es; x; e), top, s = t, alle-at(es; i; e.P(e)), es-decls(es;i;ds;da), P  Q
FDL editor aliasesecl-mng-update

origin